<html>
<head><meta charset="utf-8"><title>Relationship between lifetimes and aliasing · general · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/index.html">general</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html">Relationship between lifetimes and aliasing</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="232687414"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687414" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687414">(Apr 01 2021 at 00:41)</a>:</h4>
<p>In reasoning about my <a href="https://github.com/willcrichton/rust-slicer">program slicer</a>, I've tried to prove the following theorem.</p>
<blockquote>
<p>If <code>x : &amp;'a T</code> and <code>y : &amp;'b T</code> and it is possible that <code>x = y</code>, then <code>'a : 'b</code> or <code>'b : 'a</code></p>
</blockquote>
<p>I intuitively believe that this statement is true given how the borrow checker generates and resolves outlives constraints, but I'm struggling to come up with a formal argument. Does anyone have a better reason why? Or is there a counterexample? (note: only considering safe rust, no interior mutability)</p>



<a name="232687560"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687560" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687560">(Apr 01 2021 at 00:43)</a>:</h4>
<p><span class="user-mention" data-user-id="265377">@Will Crichton</span> I'm assuming both are live at some common point?</p>



<a name="232687603"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687603" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687603">(Apr 01 2021 at 00:43)</a>:</h4>
<p>I suppose, if that's a necessary condition?</p>



<a name="232687619"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687619" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687619">(Apr 01 2021 at 00:43)</a>:</h4>
<p>it seems like one :)</p>



<a name="232687628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687628">(Apr 01 2021 at 00:44)</a>:</h4>
<p>otherwise, you could have</p>



<a name="232687665"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687665" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687665">(Apr 01 2021 at 00:44)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="kd">let</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span><span class="w"></span>

<span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="kd">let</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">v</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="kd">let</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">v</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="232687666"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687666" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687666">(Apr 01 2021 at 00:44)</a>:</h4>
<p>What kind of equality is this? If it is just equality of values, you only need the statement <code>x == y</code> to typecheck, which means that <code>'a</code> and <code>'b</code> have a nonempty intersection</p>



<a name="232687683"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687683" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687683">(Apr 01 2021 at 00:44)</a>:</h4>
<p>that doesn't imply that one outlives the other per se</p>



<a name="232687685"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687685" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687685">(Apr 01 2021 at 00:44)</a>:</h4>
<p>Pointer equality, ie x and y are aliases.</p>



<a name="232687713"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687713" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687713">(Apr 01 2021 at 00:44)</a>:</h4>
<p>I don't think it's true</p>



<a name="232687718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687718">(Apr 01 2021 at 00:45)</a>:</h4>
<p>example:</p>



<a name="232687755"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687755" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687755">(Apr 01 2021 at 00:45)</a>:</h4>
<p>well, hmm</p>



<a name="232687776"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687776" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687776">(Apr 01 2021 at 00:45)</a>:</h4>
<p>I was thinking that maybe you can have an if/then/else where they both start on different branches</p>



<a name="232687913"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687913" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687913">(Apr 01 2021 at 00:47)</a>:</h4>
<p>The claim is a bit weird because lifetimes are a property of the type system while equality of values is a dynamic property of the operational semantics</p>



<a name="232687938"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687938" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687938">(Apr 01 2021 at 00:47)</a>:</h4>
<p>Maybe I can give the more general context. In implementing the program slicer, I'm trying to take the output of the borrow checker and compute points-to / alias information. The trouble is that the <code>BorrowSet</code> only contains information about where references are created and dropped, and not about aliases in between. </p>
<p>So my strategy is to compute aliases by with the following strategy. Given the <code>constraint_sccs</code> from the <code>RegionInferenceContext</code>, if a pointer has a lifetime <code>'a</code>, then that pointer aliases any parent in the constraint_sccs graph.</p>



<a name="232687962"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232687962" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232687962">(Apr 01 2021 at 00:47)</a>:</h4>
<p>it seems like you need to use some dynamic version of borrows, like the stacked borrow object lifetimes</p>



<a name="232688026"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688026" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688026">(Apr 01 2021 at 00:48)</a>:</h4>
<p>I _think_ this strategy is sound, but I'm trying to figure out if that's the case, and if so then what's the argument why. And it has to do with whether the outlives information computed by the borrow checker is a sufficient condition for determining the possibility of an alias.</p>



<a name="232688052"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688052" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688052">(Apr 01 2021 at 00:48)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="kd">let</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span><span class="w"></span>
<span class="kd">let</span><span class="w"> </span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="n">y</span><span class="p">);</span><span class="w"></span>
<span class="k">if</span><span class="w"> </span><span class="n">condition</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">a</span><span class="p">;</span><span class="w">  </span><span class="c1">// P1</span>
<span class="w">    </span><span class="n">y</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">a</span><span class="p">;</span><span class="w"> </span><span class="c1">// P2</span>
<span class="p">}</span><span class="w"> </span><span class="k">else</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">y</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">a</span><span class="p">;</span><span class="w"> </span><span class="c1">// P3</span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">a</span><span class="p">;</span><span class="w"> </span><span class="c1">// P4</span>
<span class="p">}</span><span class="w"></span>
<span class="nb">drop</span><span class="p">((</span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="n">y</span><span class="p">));</span><span class="w"> </span><span class="c1">// P5</span>
</code></pre></div>
<ul>
<li>lifetime of x is {P1, P2, P4, P5}</li>
<li>lifetime of y is {P2, P3, P4, P5}</li>
<li>but <code>ptr::eq(x, y)</code></li>
</ul>



<a name="232688066"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688066" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688066">(Apr 01 2021 at 00:49)</a>:</h4>
<p>that said, <span class="user-mention" data-user-id="265377">@Will Crichton</span>, have you seen my talk on polonius?</p>



<a name="232688101"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688101" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688101">(Apr 01 2021 at 00:49)</a>:</h4>
<p>it presents an alternative view of lifetimes</p>



<a name="232688104"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688104" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688104">(Apr 01 2021 at 00:49)</a>:</h4>
<p>as "origins"</p>



<a name="232688111"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688111" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688111">(Apr 01 2021 at 00:49)</a>:</h4>
<p>and I wonder if it might be of interest to you</p>



<a name="232688182"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688182" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688182">(Apr 01 2021 at 00:50)</a>:</h4>
<p><a href="https://nikomatsakis.github.io/rust-belt-rust-2019/#1">https://nikomatsakis.github.io/rust-belt-rust-2019/#1</a></p>



<a name="232688188"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688188" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688188">(Apr 01 2021 at 00:50)</a>:</h4>
<p>I don't see how <code>ptr::eq(x, y)</code> in that example?</p>



<a name="232688226"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688226" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688226">(Apr 01 2021 at 00:50)</a>:</h4>
<p><a href="https://www.youtube.com/watch?v=_agDeiWek8w">https://www.youtube.com/watch?v=_agDeiWek8w</a></p>
<div class="youtube-video message_inline_image"><a data-id="_agDeiWek8w" href="https://www.youtube.com/watch?v=_agDeiWek8w"><img src="https://i.ytimg.com/vi/_agDeiWek8w/default.jpg"></a></div>



<a name="232688230"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688230" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688230">(Apr 01 2021 at 00:50)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing/near/232688188">said</a>:</p>
<blockquote>
<p>I don't see how <code>ptr::eq(x, y)</code> in that example?</p>
</blockquote>
<p>oh, I guess that's true, lol</p>



<a name="232688234"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688234" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688234">(Apr 01 2021 at 00:51)</a>:</h4>
<p>but you can make it trivially true</p>



<a name="232688244"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688244" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688244">(Apr 01 2021 at 00:51)</a>:</h4>
<p>(fixed)</p>



<a name="232688331"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688331" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688331">(Apr 01 2021 at 00:52)</a>:</h4>
<p>also I think x should be {P1, P4, P5} and y is {P2, P3, P5}</p>



<a name="232688367"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688367" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688367">(Apr 01 2021 at 00:53)</a>:</h4>
<p>Niko I haven't seen the talk, I will check it out. And yes that's a good counter example, I agree that rejects the theorem. I think I need a different theorem then. What I really care about is whether aliases generated from _the same borrow_ satisfy that theorem.</p>



<a name="232688369"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688369" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688369">(Apr 01 2021 at 00:53)</a>:</h4>
<p>eg</p>



<a name="232688384"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688384" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688384">(Apr 01 2021 at 00:53)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="kd">let</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span><span class="w"></span>
<span class="kd">let</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">x</span><span class="p">;</span><span class="w"></span>
<span class="kd">let</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">a</span><span class="p">;</span><span class="w"></span>
</code></pre></div>



<a name="232688456"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688456" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688456">(Apr 01 2021 at 00:54)</a>:</h4>
<p>cause as I mentioned in the post above, all I'm trying to do is figure out for each pointer in the MIR, which borrow it could refer to</p>



<a name="232688485"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688485" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688485">(Apr 01 2021 at 00:55)</a>:</h4>
<p>Because of reborrows, I don't think it makes a difference:</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="kd">let</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span><span class="w"></span>
<span class="kd">let</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">b</span><span class="p">;</span><span class="w"></span>
<span class="kd">let</span><span class="w"> </span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="n">y</span><span class="p">);</span><span class="w"></span>
<span class="k">if</span><span class="w"> </span><span class="n">condition</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">a</span><span class="p">;</span><span class="w"> </span><span class="c1">// P1</span>
<span class="w">    </span><span class="n">y</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">a</span><span class="p">;</span><span class="w"> </span><span class="c1">// P2</span>
<span class="p">}</span><span class="w"> </span><span class="k">else</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">y</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">a</span><span class="p">;</span><span class="w"> </span><span class="c1">// P3</span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">a</span><span class="p">;</span><span class="w"> </span><span class="c1">// P4</span>
<span class="p">}</span><span class="w"></span>
<span class="nb">drop</span><span class="p">((</span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="n">y</span><span class="p">));</span><span class="w"> </span><span class="c1">// P5</span>
</code></pre></div>



<a name="232688520"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688520" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688520">(Apr 01 2021 at 00:55)</a>:</h4>
<p>the four <code>= a</code> lines are basically <code>x = &amp;*a</code></p>



<a name="232688721"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688721" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688721">(Apr 01 2021 at 00:59)</a>:</h4>
<p><span class="user-mention" data-user-id="271719">@Mario Carneiro</span> also a good point. I was just looking at the region SCCs for these two programs. It seems like the key fact is that <code>x</code> and <code>y</code> share <code>a</code> as a common ancestor in the SCC graph, so perhaps that's the more relevant statement.</p>



<a name="232688723"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688723" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688723">(Apr 01 2021 at 00:59)</a>:</h4>
<p>Maybe a better question is whether adding the constraint that the two lifetimes are the same or in an ordering relation would cause some programs not to typecheck. (In this example you can extend the lifetimes of <code>x</code> and <code>y</code> to match <code>a</code>.) But I would guess the answer is yes, because polonius style origins are strictly more powerful than NLL regions</p>



<a name="232688899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688899">(Apr 01 2021 at 01:01)</a>:</h4>
<p>Yes that's part of why I'm interested in proving this theorem true with respect to some notion of the "true" (or minimal) lifetimes of each pointers, as distinct from the lifetimes inferred by NLL or polonius. But I'm not sure how to precisely specify the true lifetime.</p>



<a name="232688916"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688916" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688916">(Apr 01 2021 at 01:01)</a>:</h4>
<p><span class="user-mention silent" data-user-id="265377">Will Crichton</span> <a href="#narrow/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing/near/232688456">said</a>:</p>
<blockquote>
<p>cause as I mentioned in the post above, all I'm trying to do is figure out for each pointer in the MIR, which borrow it could refer to</p>
</blockquote>
<p>this is basically <em>directly</em> what polonius computes, <span class="user-mention" data-user-id="265377">@Will Crichton</span></p>



<a name="232688924"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688924" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688924">(Apr 01 2021 at 01:01)</a>:</h4>
<p>you may want to ask questions in <a class="stream" data-stream-id="186049" href="/#narrow/stream/186049-t-compiler.2Fwg-polonius">#t-compiler/wg-polonius</a></p>



<a name="232688972"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688972" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688972">(Apr 01 2021 at 01:02)</a>:</h4>
<p>I also have some blog posts writing up the core ideas</p>



<a name="232688985"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688985" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688985">(Apr 01 2021 at 01:02)</a>:</h4>
<p>: O wow! good good</p>



<a name="232688987"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232688987" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232688987">(Apr 01 2021 at 01:02)</a>:</h4>
<p>and there's even a thesis on it :)</p>



<a name="232689009"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232689009" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232689009">(Apr 01 2021 at 01:02)</a>:</h4>
<p>well I'm trying to write an OOPSLA paper about this slicer, so I better get to it...</p>



<a name="232689035"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232689035" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232689035">(Apr 01 2021 at 01:02)</a>:</h4>
<p>written by <span class="user-mention" data-user-id="204115">@Amanda Stjerna</span> (though her name was different then, so if you go searching for it, I'm not sure how it's listed)</p>



<a name="232689172"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232689172" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232689172">(Apr 01 2021 at 01:04)</a>:</h4>
<p>I can't find a link... <span class="user-mention" data-user-id="116113">@lqd</span> may know</p>



<a name="232689589"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232689589" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232689589">(Apr 01 2021 at 01:10)</a>:</h4>
<p>there was this late draft version but I can’t quite remember if there was a later final one <a href="user_uploads/4715/ufu5BGNrkzVbV8FtkK3Tco6M/Albins-Thesis-draft-version.pdf">https://rust-lang.zulipchat.com/user_uploads/4715/ufu5BGNrkzVbV8FtkK3Tco6M/Albins-Thesis-draft-version.pdf</a></p>



<a name="232689629"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232689629" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232689629">(Apr 01 2021 at 01:10)</a>:</h4>
<p>(the link may be stale now :/)</p>



<a name="232690749"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232690749" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232690749">(Apr 01 2021 at 01:27)</a>:</h4>
<p>I’m not sure there are other public links so we may need to ask <span class="user-mention" data-user-id="204115">@Amanda Stjerna</span></p>



<a name="232691843"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232691843" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232691843">(Apr 01 2021 at 01:45)</a>:</h4>
<blockquote>
<p>all I'm trying to do is figure out for each pointer in the MIR, which borrow it could refer to</p>
</blockquote>
<p>Oh, is <em>that</em> all? <span aria-label="upside down" class="emoji emoji-1f643" role="img" title="upside down">:upside_down:</span> If you get that figured out over the weekend, that'd be a big help <span aria-label="wink" class="emoji emoji-1f609" role="img" title="wink">:wink:</span></p>



<a name="232693253"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232693253" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232693253">(Apr 01 2021 at 02:04)</a>:</h4>
<p><span class="user-mention" data-user-id="116155">@Jake Goulding</span> trying to do it conservatively! And the strategy I suggested actually seems to be working quite well: <a href="https://github.com/willcrichton/rust-slicer/blob/master/src/analysis/aliases.rs#L205">https://github.com/willcrichton/rust-slicer/blob/master/src/analysis/aliases.rs#L205</a></p>



<a name="232693731"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232693731" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232693731">(Apr 01 2021 at 02:11)</a>:</h4>
<p>Also <span class="user-mention" data-user-id="116009">@nikomatsakis</span> the talk was helpful! The concept of a loan helps clarify my struggles. For example, I was trying to reason about this program:</p>



<a name="232693859"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232693859" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232693859">(Apr 01 2021 at 02:13)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="kd">let</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span><span class="w"></span>
<span class="kd">let</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">x</span><span class="p">;</span><span class="w"></span>
<span class="kd">let</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">a</span><span class="p">;</span><span class="w"></span>
<span class="o">*</span><span class="n">a</span><span class="p">;</span><span class="w"></span>
<span class="o">*</span><span class="n">b</span><span class="p">;</span><span class="w"></span>
</code></pre></div>
<p>At first, I was thinking about this as a counterexample to my original theorem. But I noticed that Rust computes the lifetime of <code>a</code> to actually outlive <code>b</code> (presumably because <code>b = a</code> introduces such a constraint). And this broke my original mental model of "the lifetime of a reference is the live range of the pointer", and I was struggling to form a new mental model for what a lifetime really means.</p>



<a name="232741317"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232741317" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Daniel Henry-Mantilla <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232741317">(Apr 01 2021 at 11:28)</a>:</h4>
<p>Also, for any such kind of property to hold, you'll need <code>T</code> to be non-ZST; since references to unrelated ZSTs can very well compare <code>ptr</code>-equal</p>



<a name="232761579"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/232761579" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#232761579">(Apr 01 2021 at 14:04)</a>:</h4>
<p>Moving subsequent discussion on this thread to <a class="stream-topic" data-stream-id="186049" href="/#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Understanding.20the.20Polonius.20model">#t-compiler/wg-polonius &gt; Understanding the Polonius model</a></p>



<a name="234342239"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Relationship%20between%20lifetimes%20and%20aliasing/near/234342239" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing.html#234342239">(Apr 13 2021 at 15:02)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116113">lqd</span> <a href="#narrow/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing/near/232690749">said</a>:</p>
<blockquote>
<p>I’m not sure there are other public links so we may need to ask <span class="user-mention silent" data-user-id="204115">Amanda Stjerna</span></p>
</blockquote>
<p>There _should be_ but for whatever reason my university never published the final thesis. I have no idea why.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>